(declare-const x (_ BitVec 8))
(declare-const y (_ BitVec 8))
(declare-const avgu (_ BitVec 8))
(declare-const realavg Int)

(push)

; again we try to find a counterexample by asserting the premise but not the conclusion
; the conclusion is that the function computes something different than the requested value
; the result is checked in the domain of integers!
(assert (= avgu (bvadd (bvand x y) (bvlshr (bvxor x y) #x01))))
(assert (= realavg (div (+ (bv2nat x) (bv2nat y)) 2)))
(assert (not (= (bv2nat avgu) realavg)))

(check-sat)
;(get-model)

(pop)
(push)

; we do the same, but this time using arithmetic shift to see whether there is any difference
(assert (= avgu (bvadd (bvand x y) (bvashr (bvxor x y) #x01))))
(assert (= realavg (div (+ (bv2nat x) (bv2nat y)) 2)))
(assert (not (= (bv2nat avgu) realavg)))
;(check-sat)
;(get-model)